ecl{-}trans{-}halt2(${\it ds}$;${\it da}$;$A$)($n$,$L$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$ecl{-}trans{-}h($A$)($n$,ecl{-}trans{-}state($A$;$L$))